state-machine-spec{i:l}
state-machine-spec(es; C; R; F; I; O)
== X:AbsInterface(C)
== Q:EE
== B:retrace(es; Q; X)
== (Q-R-glued(es; C; (e.I(e)); I; (e,e'. (e <loc e')); X; Q)
== & Q-R-glued(es;
== & Q-R-glued(R;
== & Q-R-glued((e.F(map(e'.X(e');(retracer(B)(e)) @ [e])));
== & Q-R-glued(X;
== & Q-R-glued(Q;
== & Q-R-glued(O;
== & Q-R-glued((e,e'. (loc(e) = loc(e'))  (e <loc e')))) 

latex

---

clarification:

state-machine-spec{i:l}
state-machine-spec(es; C; R; F; I; O)
== X:AbsInterface(es;C)
== Q:es-E(es)es-E(es){i}
== B:retrace(es; Q; X)
== (Q-R-glued(es; C; (e.I(e)); I; (e,e'. es-locl(es; e; e')); X; Q)
== & Q-R-glued(es;
== & Q-R-glued(R;
== & Q-R-glued((e.F(map(e'.X(e');(retracer(B)(e)) @ [e / []])));
== & Q-R-glued(X;
== & Q-R-glued(Q;
== & Q-R-glued(O;
== & Q-R-glued((e,e'. (es-loc(es; e) = es-loc(es; e')  Id)  es-locl(es; e; e')))) 

latex

Definitions	AbsInterface(A), x:AB(x), E, , x:A. B(x), retrace(es; Q; X), P & Q, Q-R-glued(es; Ib_valtype; f; Ia; Qa; Ib; Rb), map(f;as), X(e), as @ bs, f(a), retracer(p), [car / cdr], [], x.A(x), P  Q, s = t, Id, loc(e), (e <loc e')
FDL editor aliases	state-machine-spec